Propositions as Types
Session types plan the communication sequence for concurrent programs by their direction and datatype of messages. By checking programs for compliance with these plans, the absence of communication errors or deadlocks can be guaranteed.
Propositions as Types is a powerful idea that reveals a fundamental correspondence between logic and programming. Each proposition in logic corresponds to a type in a programming language, and each proof corresponds to a program. A similar correspondence between propositions and session types can be observed, where proofs correspond to processes. This influenced several session type languages, such as Par.
Goals
Become familiar with the connection between propositions and types, and how that connection applies to propositions and sessions. Explore how the Par language is build upon the theoretical foundations of linear logic to implement a session-type language.